|
| 1: |
|
Term_sub(Case(m,xi,n),s) |
→ Frozen(m,Sum_sub(xi,s),n,s) |
| 2: |
|
Frozen(m,Sum_constant(Left),n,s) |
→ Term_sub(m,s) |
| 3: |
|
Frozen(m,Sum_constant(Right),n,s) |
→ Term_sub(n,s) |
| 4: |
|
Frozen(m,Sum_term_var(xi),n,s) |
→ Case(Term_sub(m,s),xi,Term_sub(n,s)) |
| 5: |
|
Term_sub(Term_app(m,n),s) |
→ Term_app(Term_sub(m,s),Term_sub(n,s)) |
| 6: |
|
Term_sub(Term_pair(m,n),s) |
→ Term_pair(Term_sub(m,s),Term_sub(n,s)) |
| 7: |
|
Term_sub(Term_inl(m),s) |
→ Term_inl(Term_sub(m,s)) |
| 8: |
|
Term_sub(Term_inr(m),s) |
→ Term_inr(Term_sub(m,s)) |
| 9: |
|
Term_sub(Term_var(x),Id) |
→ Term_var(x) |
| 10: |
|
Term_sub(Term_var(x),Cons_usual(y,m,s)) |
→ m |
| 11: |
|
Term_sub(Term_var(x),Cons_usual(y,m,s)) |
→ Term_sub(Term_var(x),s) |
| 12: |
|
Term_sub(Term_var(x),Cons_sum(xi,k,s)) |
→ Term_sub(Term_var(x),s) |
| 13: |
|
Term_sub(Term_sub(m,s),t) |
→ Term_sub(m,Concat(s,t)) |
| 14: |
|
Sum_sub(xi,Id) |
→ Sum_term_var(xi) |
| 15: |
|
Sum_sub(xi,Cons_sum(psi,k,s)) |
→ Sum_constant(k) |
| 16: |
|
Sum_sub(xi,Cons_sum(psi,k,s)) |
→ Sum_sub(xi,s) |
| 17: |
|
Sum_sub(xi,Cons_usual(y,m,s)) |
→ Sum_sub(xi,s) |
| 18: |
|
Concat(Concat(s,t),u) |
→ Concat(s,Concat(t,u)) |
| 19: |
|
Concat(Cons_usual(x,m,s),t) |
→ Cons_usual(x,Term_sub(m,t),Concat(s,t)) |
| 20: |
|
Concat(Cons_sum(xi,k,s),t) |
→ Cons_sum(xi,k,Concat(s,t)) |
| 21: |
|
Concat(Id,s) |
→ s |
|
There are 23 dependency pairs:
|
| 22: |
|
Term_sub#(Case(m,xi,n),s) |
→ Frozen#(m,Sum_sub(xi,s),n,s) |
| 23: |
|
Term_sub#(Case(m,xi,n),s) |
→ Sum_sub#(xi,s) |
| 24: |
|
Frozen#(m,Sum_constant(Left),n,s) |
→ Term_sub#(m,s) |
| 25: |
|
Frozen#(m,Sum_constant(Right),n,s) |
→ Term_sub#(n,s) |
| 26: |
|
Frozen#(m,Sum_term_var(xi),n,s) |
→ Term_sub#(m,s) |
| 27: |
|
Frozen#(m,Sum_term_var(xi),n,s) |
→ Term_sub#(n,s) |
| 28: |
|
Term_sub#(Term_app(m,n),s) |
→ Term_sub#(m,s) |
| 29: |
|
Term_sub#(Term_app(m,n),s) |
→ Term_sub#(n,s) |
| 30: |
|
Term_sub#(Term_pair(m,n),s) |
→ Term_sub#(m,s) |
| 31: |
|
Term_sub#(Term_pair(m,n),s) |
→ Term_sub#(n,s) |
| 32: |
|
Term_sub#(Term_inl(m),s) |
→ Term_sub#(m,s) |
| 33: |
|
Term_sub#(Term_inr(m),s) |
→ Term_sub#(m,s) |
| 34: |
|
Term_sub#(Term_var(x),Cons_usual(y,m,s)) |
→ Term_sub#(Term_var(x),s) |
| 35: |
|
Term_sub#(Term_var(x),Cons_sum(xi,k,s)) |
→ Term_sub#(Term_var(x),s) |
| 36: |
|
Term_sub#(Term_sub(m,s),t) |
→ Term_sub#(m,Concat(s,t)) |
| 37: |
|
Term_sub#(Term_sub(m,s),t) |
→ Concat#(s,t) |
| 38: |
|
Sum_sub#(xi,Cons_sum(psi,k,s)) |
→ Sum_sub#(xi,s) |
| 39: |
|
Sum_sub#(xi,Cons_usual(y,m,s)) |
→ Sum_sub#(xi,s) |
| 40: |
|
Concat#(Concat(s,t),u) |
→ Concat#(s,Concat(t,u)) |
| 41: |
|
Concat#(Concat(s,t),u) |
→ Concat#(t,u) |
| 42: |
|
Concat#(Cons_usual(x,m,s),t) |
→ Term_sub#(m,t) |
| 43: |
|
Concat#(Cons_usual(x,m,s),t) |
→ Concat#(s,t) |
| 44: |
|
Concat#(Cons_sum(xi,k,s),t) |
→ Concat#(s,t) |
|
The approximated dependency graph contains 3 SCCs:
{38,39},
{34,35}
and {22,24-33,36,37,40-44}.